\section{CCAT Class}
\label{Section:ComputerControlledAutomaticTransmission}
The \emph{ComputerControlledAutomaticTransmission} class is formalized thanks to the code reported in Listing~\ref{Code:ComputerControlledAutomaticTransmission} while Figure~\ref{Figure:CCAT} shows the \emph{big picture} of our complete designed.

\lstinputlisting[language=TRIO,tabsize=4,numbers=left,numberstyle=\small,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=ComputerControlledAutomaticTransmission.trio,label=Code:ComputerControlledAutomaticTransmission]{../trio/ComputerControlledAutomaticTransmission.trio}

\thispagestyle{empty}
\begin{figure}[!p]
\vspace{-3 cm}
\centerline{\includegraphics[scale=0.8,angle=-90]{images/CCAT.pdf}}
\caption{Computer Controller Automatic Transmission}
\label{Figure:CCAT}
\end{figure}

\newpage
Due to the fact that a complete \emph{TRIO} specification is undecidable we have decided to focus our verification process only on a subset of our system, in particular we have dealt with the Hydraulic System, described in Section~\ref{Section:HydraulicSystem}, and with the Planetary Gear Set, described in Section~\ref{Section:PlanetaryGearSet}.

The \emph{decidable TRIO} specification which further translated in a \emph{ProMeLa} specification thanks to \emph{TRIO2ProMeLa} and then passed to \emph{Spin} is reported in Listing~\ref{Code:ComputerControlledAutomaticTransmission2}.

\lstinputlisting[language=TRIO,tabsize=4,numbers=left,numberstyle=\small,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=ComputerControlledAutomaticTransmission.trio,label=Code:ComputerControlledAutomaticTransmission2]{../t2p/ComputerControlledAutomaticTransmission.trio}

More details can be found at this web page \url{http://code.google.com/p/ccat/source/browse/#svn/trunk/t2p}.

The same decidable TRIO specification reported in Listings~\ref{Code:ComputerControlledAutomaticTransmission2} has been ported - with few arrangements - in \emph{Zot} and the result is shown in Listings~\ref{Code:ComputerControlledAutomaticTransmission3}.

\lstinputlisting[language=Zot,tabsize=4,numbers=left,numberstyle=\small,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=ComputerControlledAutomaticTransmission.lisp,label=Code:ComputerControlledAutomaticTransmission3]{../zot/ComputerControlledAutomaticTransmission.lisp}
